Problem:
 twoto(0(x1)) -> p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
 twoto(s(x1)) ->
 p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
 twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
 twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
 p(p(s(x1))) -> p(x1)
 p(s(x1)) -> x1
 p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
 0(x1) -> x1

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {5,4,3,2}
   transitions:
    s1(65) -> 66*
    s1(60) -> 61*
    s1(55) -> 56*
    s1(50) -> 51*
    s1(45) -> 46*
    s1(40) -> 41*
    s1(35) -> 36*
    s1(67) -> 68*
    s1(62) -> 63*
    s1(74) -> 75*
    s1(69) -> 70*
    s1(49) -> 50*
    s1(44) -> 45*
    s1(39) -> 40*
    s1(66) -> 67*
    s1(56) -> 57*
    s1(51) -> 52*
    s1(68) -> 69*
    s1(38) -> 39*
    s1(33) -> 34*
    p1(70) -> 71*
    p1(72) -> 73*
    p1(57) -> 58*
    p1(52) -> 53*
    p1(47) -> 48*
    p1(42) -> 43*
    p1(54) -> 55*
    p1(34) -> 35*
    p1(71) -> 72*
    p1(61) -> 62*
    p1(46) -> 47*
    p1(41) -> 42*
    p1(36) -> 37*
    p1(73) -> 74*
    p1(63) -> 64*
    p1(58) -> 59*
    p1(53) -> 54*
    p1(43) -> 44*
    twice1(64) -> 65*
    twice1(48) -> 49*
    twoto1(37) -> 38*
    p2(122) -> 123*
    p2(102) -> 103*
    p2(124) -> 125*
    p2(114) -> 115*
    p2(104) -> 105*
    p2(94) -> 95*
    p2(116) -> 117*
    p2(96) -> 97*
    p2(110) -> 111*
    twoto0(1) -> 2*
    00(1) -> 5*
    p0(1) -> 4*
    s0(1) -> 1*
    twice0(1) -> 3*
    1 -> 5,4,33
    33 -> 35*
    35 -> 37*
    37 -> 60*
    38 -> 117*
    39 -> 95,43,116
    40 -> 42,94
    44 -> 111,48
    45 -> 47,110
    49 -> 115,55,97
    50 -> 103,54,114
    51 -> 53,102
    55 -> 97*
    56 -> 58,96
    59 -> 38,2
    60 -> 62*
    62 -> 64*
    66 -> 125,74
    67 -> 123,73,124
    68 -> 105,122
    69 -> 71,104
    75 -> 65,3
    95 -> 43*
    97 -> 59*
    103 -> 54*
    105 -> 72*
    111 -> 48*
    115 -> 55*
    117 -> 44*
    123 -> 73*
    125 -> 74*
  problem:
   
  Qed